FDL - Step of Proof: nth_tl_append

Step of Proof: nth_tl_append

Inference at * 2 1
Iof proof for Lemma nth tl append:

1. T : Type
2. T List
3. u : T
4. v : T List
5. bs : T List
6. nth_tl(||v||;v @ bs) ~ bs

nth_tl(||v||+1;[u / (v @ bs)]) ~ bs

by ((((RecUnfold `nth_tl` 0)

CollapseTHEN ((((if (0

C) =0 then SplitOnConclITE else SplitOnHypITE (0))

)

CollapseTHEN (Reduce 0))

))

)

CoCollapseTHEN ((Try ((Complete (Auto'))

))

))

C1:

C1: 7. 0 < (||v||+1)

C1:

nth_tl((||v||+1) - 1;v @ bs) ~ bs

C.

Definitions left + right, Unit, , p q, p q, p q, [d], a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), A, P Q, T, P Q, P & Q, x:A B(x), tl(l), tt, [car / cdr], A B, True, b, b, i <z j, , i z j, ff, SQType(T), x:A. B(x), P Q, x:AB(x), {T}, i j , nth_tl(n;as), n - m, n+m, ||as||, #$n, as @ bs, a < b, s ~ t, Type, type List, , s = t, t T

Lemmas eqtt to assert, assert of le int, iff transitivity, eqff to assert, iff wf, rev implies wf, squash wf, true wf, bnot of le int, assert of lt int, le int wf, length wf1, le wf, non neg length, bool wf, lt int wf, assert wf, bnot wf, append wf, nth tl wf, guard wf